STRATEGY =
(LAMBDA (X) (SUPPORT X)) 
SUPPORT-SET-IS: 
¬R(D(U,D(U,D(U,THM39))),D(U,THM39)) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =T
DEPTH-BOUND =3
LENGTH-BOUND =2

PARMODULATE =T
EQUAL-SYMBOL =R
PAR-DEPTH-BOUND =3
ELAPSED-TIME =54149

NIL 1 2
1 ¬R(O,O) 3 4
2 R(X1,X1) AXIOM 6
3 ¬LE(D(U,THM39),D(U,THM39)) 5 10
4 LE(X1,X2) ¬R(D(X1,X2),O) AXIOM 2
5 ¬LE(D(U,D(U,THM39)),THM39) ¬LE(D(U,THM39),D(U,THM39)) 7 12
7 ¬LE(D(U,D(U,THM39)),THM39) ¬LE(D(U,D(U,THM39)),D(U,D(U,THM39))) 9 10
9 ¬LE(D(U,D(U,D(U,THM39))),D(U,THM39)) ¬LE(D(U,D(U,THM39)),THM39) 11 12
10 LE(D(X1,X2),X3) ¬LE(D(X1,X3),X2) AXIOM 9
11 ¬LE(D(U,THM39),D(U,D(U,D(U,THM39)))) ¬LE(D(U,D(U,D(U,THM39))),D(U,THM39)) 13 14
12 LE(D(X1,X2),D(X1,X3)) ¬LE(X3,X2) AXIOM 10
13 R(X1,X2) ¬LE(X2,X1) ¬LE(X1,X2) AXIOM 7
14 ¬R(D(U,D(U,D(U,THM39))),D(U,THM39)) AXIOM -13